#| Certification code:

(certify-book "my-member-lemmas" 0 nil)

|#

(in-package "ACL2")

;;Lemas y definiciones previas:

(include-book "dg-list")

(defun cmp-d-ls-dgop-do (d p rsl)
  (cond ((endp p) (reverse rsl))
        ((< d (car p)) (cmp-d-ls-dgop-do d (cdr p) (cons (1- (car p)) rsl)))
        ((and (<= 0 (- d (car p)))
              (<= (- d (car p)) 1)) (append (reverse rsl) (rest p)))
        (t (cmp-d-ls-dgop-do (1- d) (cdr p) (cons (car p) rsl)))
        )
  )

(defun cmp-d-ls-d-do (d p)
  (cond ((endp p) d)
	((< d (car p)) (cmp-d-ls-d-do d (cdr p) ))
        ((and (<= 0 (- d (car p)))
              (<= (- d (car p)) 1)) nil)
        (t (cmp-d-ls-d-do (1- d) (cdr p)))
        )
  )

(defun cmp-d-ls (d ls)
  (cmp-d-ls-dgop-do d ls nil)
  )


(encapsulate
 ()
 
 (local
  (defthm append-revappend
      (equal (append (revappend l1 l2) l3)
             (revappend l1 (append l2 l3)))))
 
 (local
  (defthm revappend-append
      (equal (revappend (append ls1 ls2) ls3)
             (revappend ls2 (revappend ls1 ls3)))))
 
 (local
  (defthm cmp-d-ls-dgop-do-append-rsl
      (implies (and (true-listp rsl1)
                    (true-listp rsl2))
               (equal (cmp-d-ls-dgop-do s p (append rsl1 rsl2))
                      (append (reverse rsl2) (cmp-d-ls-dgop-do s p rsl1))))
    :rule-classes nil))
 
 (local
  (defthm cmp-d-ls-dgop-do-nil-rsl
      (implies (and (true-listp rsl1)
                    (not (endp rsl1)))
               (equal (cmp-d-ls-dgop-do s p rsl1)
                      (append (reverse rsl1) (cmp-d-ls-dgop-do s p nil))))
    :hints (("Goal" :use (:instance cmp-d-ls-dgop-do-append-rsl
                                    (rsl1 nil)
                                    (rsl2 rsl1))))))
 
 (defthm cmp-d-ls-recursive
     (equal (cmp-d-ls d ls)
            (cond ((endp ls) nil)
                  ((< d (car ls)) (cons (1- (car ls)) (cmp-d-ls d (cdr ls))))
                  ((and (<= 0 (- d (car ls)))
                        (<= (- d (car ls)) 1)) (cdr ls))              
                  (t (cons (car ls) (cmp-d-ls (1- d) (cdr ls))))
                  ))
   :rule-classes :definition)
 
 (defun cmp-d-ls-induct (d ls)
   (cond 
	 ((endp ls) nil)
         ((< d (car ls)) (cons (1- (car ls)) (cmp-d-ls-induct d (cdr ls))))
         ((and (<= 0 (- d (car ls)))
               (<= (- d (car ls)) 1)) (cdr ls))              
         (t (cons (car ls) (cmp-d-ls-induct (- d 1) (cdr ls))))
         )
   )
 
 (in-theory (disable cmp-d-ls))
 
 )

(defthm cmp-d-ls-cmp-d-ls-induct
    (equal (cmp-d-ls i ls)
           (cmp-d-ls-induct i ls)))

;; Notar que si > j (1+ (car ls)) entonces cmp-d-ls-induct j ls es ls

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help1
  (implies (and (natp j) (dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (equal (cmp-d-ls-induct j ls)
		  ls)))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help2
  (implies (and (natp j) (dgl-p ls)
		(>=  j (car ls))
		(not (endp ls))
		(not (and (<= 0 (- j (car ls)))
			  (<= (- j (car ls)) 1)))
		) 
	   (equal (cmp-d-ls-induct j ls)
		  ls)))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help1-bis
  (implies (and (natp j) (dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (equal (cmp-d-ls-d-do j ls)
		  (- j (len ls)))))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help2-bis
  (implies (and (natp j) (dgl-p ls)
		(>=  j (car ls))
		(not (endp ls))
		(not (and (<= 0 (- j (car ls)))
			  (<= (- j (car ls)) 1)))
		) 
	   (equal (cmp-d-ls-d-do j ls)
		  (- j (len ls)))))

(defthm dgl-p-cmp-d-ls
    (implies (and (dgl-p dgl)
                  (natp n))
             (dgl-p (cmp-d-ls n dgl)))
  :hints (("Goal" :induct (cmp-d-ls-induct n dgl))))

(defthm cmp-d-ls-d-do-not-nil
  (implies (and (natp j) 
		(dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (cmp-d-ls-d-do j ls)))


;; My-member definitions

(defun my-member (i ls)
  (if (endp ls)
      nil
    (if (and (<= 0 (- i (car ls)))
	     (<= (- i (car ls)) 1))
	t
      (my-member i (cdr ls)))))



(defun my-member-2 (i ls)
  (if (endp ls)
      nil
    (if (= 0 (- i (car ls)))
	t
      (my-member-2 i (cdr ls)))))

(defun my-member-3 (i ls)
  (if (endp ls)
      nil
    (if (= 1 (- i (car ls)))
	t
      (my-member-3 i (cdr ls)))))

(defthm my-member-1-implies-my-member-2
  (implies (and (natp i)
		(dgl-p ls)
		(my-member i ls))
	   (or (my-member-2 i ls)
	       (my-member-3 i ls)))
:rule-classes nil
)


(defthm my-member-1-implies-my-member-2-b
  (implies (and (natp i)
		(dgl-p ls)
		)
	   (equal (my-member-2 i ls)
		  (my-member-3 (+ i 1) ls)
	   )))


(defthm my-member-implies-face-do-null 
  (implies (and (natp i)
		(dgl-p ls)
		(my-member i ls))
	   (null (cmp-d-ls-d-do i ls)))
:hints (("Goal" :induct (cmp-d-ls-d-do i ls)
))
)

(defthm not-my-member-implies-face-do-not-null 
  (implies (and (natp i)
		(dgl-p ls)
		(not (my-member i ls)))
	   (cmp-d-ls-d-do i ls))
:hints (("Goal" :induct (cmp-d-ls-d-do i ls)
))
)

(defthm face-do-null-implies-not-my-member
  (implies (and (natp i)
		(dgl-p ls)
		(cmp-d-ls-d-do i ls)
		)
	   (not (my-member i ls)))
:hints (("Goal" :induct (cmp-d-ls-d-do i ls)
))
)

(defthm face-do-if-null-implies-not-my-member
  (implies (and (natp i)
		(dgl-p ls)
		(null (cmp-d-ls-d-do i ls))
		)
	   (my-member i ls))
:hints (("Goal" :induct (cmp-d-ls-d-do i ls)))
)


;;Tenemos 4 casos:

;;Caso 1:
;;-> (null (cmp-d-ls-d-do j ls))
;;-> (null (cmp-d-ls-d-do i ls))

;;i<j-1

(defthm lemma1
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(> (- j 1) i)
		)
	   (my-member i (cmp-d-ls j ls))
	   )
)

(defthm lemma1-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))		
		(> j i)
		(> (- j 1) i)
		)
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls)))
	   )
 :hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls j ls)))
		 )))
)




(defthm lemma2
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(> (- j 1) i))
	   (my-member (- j 1) (cmp-d-ls i ls))
	   )
)


(defthm lemma2-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))		
		(> j i)
		(> (- j 1) i)
		)
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls)))
	   )
 :hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls i ls)))
		 )))
)


;; i=j-1

(defthm lemma1.0
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(not (my-member-3 i ls))
		)
	   (not (my-member i (cmp-d-ls j ls)))	   
	   )
)

(defthm lemma1.0-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(not (my-member-3 i ls))
		)
	   (cmp-d-ls-d-do i (cmp-d-ls j ls)))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1.0)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma2.0
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(not (my-member-3 i ls))
		)
	   (not (my-member (- j 1) (cmp-d-ls i ls)))	   
	   )
)

(defthm lemma2.0-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(not (my-member-3 i ls))
		)
	   (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls)))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2.0)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null (i (- j 1))
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma1.0-lemma2.0-a
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(not (my-member-3 i ls))
		)
	   (equal
	    (cmp-d-ls-d-do i (cmp-d-ls j ls))
	    (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls)))))



(defthm lemma1.1
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(not (my-member-2 i ls))
		(my-member-3 i ls)
		)
	   (my-member i (cmp-d-ls j ls))	   
	   )
)

(defthm lemma1.1-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(not (my-member-2 i ls))
		(my-member-3 i ls)
		)
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1.1)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma2.1
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(not (my-member-2 i ls))
		(my-member-3 i ls)
		)
	   (my-member (- j 1) (cmp-d-ls i ls))	   
	   )
)

(defthm lemma2.1-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(not (my-member-2 i ls))
		(my-member-3 i ls)
		)
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2.1)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )



(defthm lemma1.2
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(not(my-member-3 i ls))
		)
	   (my-member i (cmp-d-ls j ls))	   
	   )
)

(defthm lemma1.2-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(not(my-member-3 i ls))
		)
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1.2)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma2.2
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(not(my-member-3 i ls))
		)
	   (my-member (- j 1) (cmp-d-ls i ls))	   
	   )
)

(defthm lemma2.2-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(not(my-member-3 i ls))
		)
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2.2)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma1.3
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (my-member i (cmp-d-ls j ls))	   
	   )
)

(defthm lemma1.3-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1.3)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma2.3
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (my-member (- j 1) (cmp-d-ls i ls))	   
	   )
)

(defthm lemma2.3-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(my-member-3 i ls)	
		)
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2.3)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )





(defthm lemma1.4
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (my-member i (cmp-d-ls j ls))	   
	   )
)

(defthm lemma1.4-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1.4)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma2.4
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (my-member (- j 1) (cmp-d-ls i ls))	   
	   )
)

(defthm lemma2.4-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(my-member-3 i ls)	
		)
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2.4)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm case/6-help
  (implies (and (natp i) (dgl-p ls)
		(not (my-member-2 i ls))
		(not (my-member-3 i ls)))
	   (not (my-member i ls))))

(defthm case/8-help
  (implies (and (natp j) (dgl-p ls)
		(not (my-member-2 j ls))
		(not (my-member-2 (- j 1) ls)))
	   (not (my-member j ls)))
)




;;Caso 2:
;;-> (cmp-d-ls-d-do j ls)
;;-> (cmp-d-ls-d-do i ls)



(defthm lemma3
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member j ls))
		(not (my-member i ls))
		(> j i))
	   (not (my-member (- j 1) (cmp-d-ls i ls)))
	   )
)



(defthm lemma3-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance face-do-null-implies-not-my-member (i j))
		 (:instance face-do-null-implies-not-my-member (i i))
		 (:instance lemma3)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null (i (- j 1))
			    (ls (cmp-d-ls i ls)))
		 ))))

(defthm lemma11
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (equal (cmp-d-ls-d-do i ls)
		  (cmp-d-ls-d-do i (cmp-d-ls j ls) )
	    )
  ))

(in-theory (disable lemma11))

(defthm lemma4
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member j ls))
		(not (my-member i ls))
		(> j i))
	   (not (my-member i (cmp-d-ls j ls)))
	   )
)


(defthm lemma4-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (cmp-d-ls-d-do i (cmp-d-ls j ls)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance face-do-null-implies-not-my-member (i j))
		 (:instance face-do-null-implies-not-my-member (i i))
		 (:instance lemma4)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null
			    (ls (cmp-d-ls j ls)))
		 ))))


(defthm lemma12.0
  (implies (and (natp j) (dgl-p ls)
		(> j (+ (car ls) 1))
		(> (- j 1) (+ (car ls) 1))
		(not (endp ls))
		) 
	   (equal (- (cmp-d-ls-d-do j ls) 1)
		  (cmp-d-ls-d-do (- j 1) (cmp-d-ls (- j 1) ls)
				 ))))


(defthm lemma12-1
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (< (cmp-d-ls-d-do i (cmp-d-ls j ls))
	      (cmp-d-ls-d-do j ls))
  )
:hints (("Goal" :induct (cmp-d-ls-d-do j ls))))



(defthm lemma12
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (equal (- (cmp-d-ls-d-do j ls) 1)
		  (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls) )   
	    )
  )
:hints (("Goal" :induct (cmp-d-ls-d-do j ls))))


;;Caso 3:
;;-> (null (cmp-d-ls-d-do j ls))
;;-> (cmp-d-ls-d-do i ls)

(defthm lemma5
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(not (my-member i ls))
		(> j i))
	   (my-member (- j 1) (cmp-d-ls i ls))))


(defthm lemma5-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance face-do-if-null-implies-not-my-member (i j))
		 (:instance face-do-null-implies-not-my-member (i i))
		 (:instance lemma5)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls i ls)))
		 ))))



(defthm lemma6-1
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member i ls))
		(my-member j ls)
		(> j i)
		(< i (- j 1))
		)
	   (not (my-member i (cmp-d-ls j ls)))
	   )
)


(defthm lemma6-2
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member i ls))
		(my-member j ls)
		(> j i)
		(= i (- j 1))
		)
	   (not (my-member i (cmp-d-ls j ls)))
	   )
)

(defthm lemma6
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member i ls))
		(my-member j ls)
		(> j i)
		)
	   (not (my-member i (cmp-d-ls j ls)))
	   )
:hints (("Goal" :do-not-induct t
	 :use ((:instance lemma6-2)
	       (:instance lemma6-1))))
)

(defthm lemma6-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do i ls)
		(null (cmp-d-ls-d-do j ls))
		(> j i)
		)
	   (cmp-d-ls-d-do i (cmp-d-ls j ls) )
	   )
:hints (("Goal" :do-not-induct t
	 :use ((:instance face-do-if-null-implies-not-my-member (i j))
		 (:instance face-do-null-implies-not-my-member (i i))
		 (:instance lemma6)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null
			    (ls (cmp-d-ls i ls)))
		 )))
)

(defthm lemma10
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do i ls)
		(null (cmp-d-ls-d-do j ls))
		(> j i)
		)
	   (equal (cmp-d-ls-d-do i (cmp-d-ls j ls) )
		  (cmp-d-ls-d-do i ls)
	   )
))


;;Caso 4:
;;-> (cmp-d-ls-d-do j ls)
;;-> (null (cmp-d-ls-d-do i ls))

(defthm lemma7
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member j ls))
		(my-member i ls)
		(> j i))
	   (not (my-member (- j 1) (cmp-d-ls i ls)))))

(defthm lemma7-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(null (cmp-d-ls-d-do i ls))
		(> j i))
	   (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance face-do-null-implies-not-my-member (i j))
		 (:instance face-do-if-null-implies-not-my-member (i i))
		 (:instance lemma7)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null (i (- j 1))
			    (ls (cmp-d-ls i ls)))
		 ))))

(defthm lemma8
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member j ls))
		(my-member i ls)
		(> j i))
	   (my-member i (cmp-d-ls j ls))))

(defthm lemma8-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(null (cmp-d-ls-d-do i ls))
		(> j i))
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance face-do-null-implies-not-my-member (i j))
		 (:instance face-do-if-null-implies-not-my-member (i i))
		 (:instance lemma8)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls i ls)))
		 ))))

(defthm lemma9
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(null (cmp-d-ls-d-do i ls))
		(> j i))
	   (equal (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))
		  (cmp-d-ls-d-do j ls))))













